Separation Logic-Based Program Verifier Using Z3
Separation Logic is a formalism used for reasoning about programs that manipulate pointers and dynamically allocated memory (heap). It allows for modular verification by reasoning about disjoint memory regions and specifying the expected behavior of programs via preconditions and postconditions. This modular approach enables the verification of individual program components in isolation, ensuring that they meet their specified contracts without interference from other parts of the system.
Examples of semi-automated deductive program verifiers based on separation logic include:
- VeriFast: A verifier for C and Java programs that uses separation logic to reason about memory safety.
- Viper: A verification infrastructure designed for a variety of programming languages, providing expressive reasoning about heap-manipulating programs.
- VerCors: A verifier aimed at reasoning about concurrent programs using separation logic.
Goal
The goal of this project is to develop a deductive program verifier based on separation logic for a simple imperative programming language. You can define your own WHILE/IMP-style language or use a subset of C that supports basic operations, pointers, and heap manipulation.
To achieve this, your project should focus on the following tasks:
- Language Design:
- Define a simple imperative programming language with basic constructs (e.g., assignments, conditionals, loops) and support for pointers and heap memory allocation & deallocation.
- Optionally, you can choose a small subset of an existing language like C.
- Define a simple imperative programming language with basic constructs (e.g., assignments, conditionals, loops) and support for pointers and heap memory allocation & deallocation.
- Program Annotation:
Extend your language to allow annotations with preconditions and postconditions expressed in separation logic. These annotations will specify the required properties of the program, such as memory safety and functional correctness.
- Symbolic Execution:
- Implement a symbolic execution engine for the chosen language. This engine will simulate the program’s execution symbolically, meaning it will track logical variables and conditions instead of concrete values.
- The symbolic execution should generate verification conditions (VCs)—logical propositions that must be proven true for the program to be verified.
- Implement a symbolic execution engine for the chosen language. This engine will simulate the program’s execution symbolically, meaning it will track logical variables and conditions instead of concrete values.
- Verification Condition Generation and Solving:
- Translate the verification conditions generated by symbolic execution into logical formulas that can be passed to an SMT solver.
- Use an SMT solver like Z3 to automatically check the correctness of the generated verification conditions. Z3 is a highly expressive solver that supports various logical theories, making it well-suited for verifying conditions generated from separation logic.
- Translate the verification conditions generated by symbolic execution into logical formulas that can be passed to an SMT solver.
This project combines key aspects of formal verification, symbolic execution, and the use of powerful SMT solvers to ensure the correctness of heap-manipulating programs. We expect this project to be challenging but a lot of fun.
Starting Points
- Separation Logic and Concurrency (OPLSS 2016)
- Symbolic Execution Lecture
- Types and Programming Languages Available at TUD's library. Maybe the most popular introduction to formal programming language semantics.
- VeriFast Program verifier for C based on separation logic, if you encounter problems with a nightly build, choose a stable, named release instead
- Dafny Program verifier based on dynamic frames
- Viper Permission-based program verifier
- Z3 powerful SMT solver